The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

min(x, 0) → 0 [1]
min(0, y) → 0 [1]
min(s(x), s(y)) → s(min(x, y)) [1]
max(x, 0) → x [1]
max(0, y) → y [1]
max(s(x), s(y)) → s(max(x, y)) [1]
-(x, 0) → x [1]
-(s(x), s(y)) → -(x, y) [1]
gcd(s(x), s(y)) → gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y))) [1]

Rewrite Strategy: INNERMOST

(3) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID) transformation)

Renamed defined symbols to avoid conflicts with arithmetic symbols:

- => minus

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

min(x, 0) → 0 [1]
min(0, y) → 0 [1]
min(s(x), s(y)) → s(min(x, y)) [1]
max(x, 0) → x [1]
max(0, y) → y [1]
max(s(x), s(y)) → s(max(x, y)) [1]
minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
gcd(s(x), s(y)) → gcd(minus(s(max(x, y)), s(min(x, y))), s(min(x, y))) [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

min(x, 0) → 0 [1]
min(0, y) → 0 [1]
min(s(x), s(y)) → s(min(x, y)) [1]
max(x, 0) → x [1]
max(0, y) → y [1]
max(s(x), s(y)) → s(max(x, y)) [1]
minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
gcd(s(x), s(y)) → gcd(minus(s(max(x, y)), s(min(x, y))), s(min(x, y))) [1]

The TRS has the following type information:

min :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s max :: 0:s → 0:s → 0:s minus :: 0:s → 0:s → 0:s gcd :: 0:s → 0:s → gcd

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

minus(v0, v1) → null_minus [0]
gcd(v0, v1) → null_gcd [0]
min(v0, v1) → null_min [0]
max(v0, v1) → null_max [0]

And the following fresh constants:

null_minus, null_gcd, null_min, null_max

(8) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: min(x, 0) → 0 [1] min(0, y) → 0 [1] min(s(x), s(y)) → s(min(x, y)) [1] max(x, 0) → x [1] max(0, y) → y [1] max(s(x), s(y)) → s(max(x, y)) [1] minus(x, 0) → x [1] minus(s(x), s(y)) → minus(x, y) [1] gcd(s(x), s(y)) → gcd(minus(s(max(x, y)), s(min(x, y))), s(min(x, y))) [1] minus(v0, v1) → null_minus [0] gcd(v0, v1) → null_gcd [0] min(v0, v1) → null_min [0] max(v0, v1) → null_max [0] The TRS has the following type information: min :: 0:s:null_minus:null_min:null_max → 0:s:null_minus:null_min:null_max → 0:s:null_minus:null_min:null_max 0 :: 0:s:null_minus:null_min:null_max s :: 0:s:null_minus:null_min:null_max → 0:s:null_minus:null_min:null_max max :: 0:s:null_minus:null_min:null_max → 0:s:null_minus:null_min:null_max → 0:s:null_minus:null_min:null_max minus :: 0:s:null_minus:null_min:null_max → 0:s:null_minus:null_min:null_max → 0:s:null_minus:null_min:null_max gcd :: 0:s:null_minus:null_min:null_max → 0:s:null_minus:null_min:null_max → null_gcd null_minus :: 0:s:null_minus:null_min:null_max null_gcd :: null_gcd null_min :: 0:s:null_minus:null_min:null_max null_max :: 0:s:null_minus:null_min:null_max Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
null_minus => 0
null_gcd => 0
null_min => 0
null_max => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

gcd(z, z') -{ 1 }→ gcd(minus(1 + max(x, y), 1 + min(x, y)), 1 + min(x, y)) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
gcd(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
max(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
max(z, z') -{ 1 }→ y :|: y >= 0, z = 0, z' = y
max(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
max(z, z') -{ 1 }→ 1 + max(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
min(z, z') -{ 1 }→ 0 :|: x >= 0, z = x, z' = 0
min(z, z') -{ 1 }→ 0 :|: y >= 0, z = 0, z' = y
min(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
min(z, z') -{ 1 }→ 1 + min(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

(11) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1),0,[min(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[max(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(min(V, V1, Out),1,[],[Out = 0,V2 >= 0,V = V2,V1 = 0]). eq(min(V, V1, Out),1,[],[Out = 0,V3 >= 0,V = 0,V1 = V3]). eq(min(V, V1, Out),1,[min(V4, V5, Ret1)],[Out = 1 + Ret1,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(max(V, V1, Out),1,[],[Out = V6,V6 >= 0,V = V6,V1 = 0]). eq(max(V, V1, Out),1,[],[Out = V7,V7 >= 0,V = 0,V1 = V7]). eq(max(V, V1, Out),1,[max(V8, V9, Ret11)],[Out = 1 + Ret11,V1 = 1 + V9,V8 >= 0,V9 >= 0,V = 1 + V8]). eq(minus(V, V1, Out),1,[],[Out = V10,V10 >= 0,V = V10,V1 = 0]). eq(minus(V, V1, Out),1,[minus(V11, V12, Ret)],[Out = Ret,V1 = 1 + V12,V11 >= 0,V12 >= 0,V = 1 + V11]). eq(gcd(V, V1, Out),1,[max(V13, V14, Ret001),min(V13, V14, Ret011),minus(1 + Ret001, 1 + Ret011, Ret0),min(V13, V14, Ret111),gcd(Ret0, 1 + Ret111, Ret2)],[Out = Ret2,V1 = 1 + V14,V13 >= 0,V14 >= 0,V = 1 + V13]). eq(minus(V, V1, Out),0,[],[Out = 0,V15 >= 0,V16 >= 0,V = V15,V1 = V16]). eq(gcd(V, V1, Out),0,[],[Out = 0,V17 >= 0,V18 >= 0,V = V17,V1 = V18]). eq(min(V, V1, Out),0,[],[Out = 0,V19 >= 0,V20 >= 0,V = V19,V1 = V20]). eq(max(V, V1, Out),0,[],[Out = 0,V21 >= 0,V22 >= 0,V = V21,V1 = V22]). input_output_vars(min(V,V1,Out),[V,V1],[Out]). input_output_vars(max(V,V1,Out),[V,V1],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [max/3]
1. recursive : [min/3]
2. recursive : [minus/3]
3. recursive : [gcd/3]
4. non_recursive : [start/2]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into max/3
1. SCC is partially evaluated into min/3
2. SCC is partially evaluated into minus/3
3. SCC is partially evaluated into gcd/3
4. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations max/3
* CE 13 is refined into CE [19]
* CE 10 is refined into CE [20]
* CE 11 is refined into CE [21]
* CE 12 is refined into CE [22]


### Cost equations --> "Loop" of max/3
* CEs [22] --> Loop 14
* CEs [19] --> Loop 15
* CEs [20] --> Loop 16
* CEs [21] --> Loop 17

### Ranking functions of CR max(V,V1,Out)
* RF of phase [14]: [V,V1]

#### Partial ranking functions of CR max(V,V1,Out)
* Partial RF of phase [14]:
- RF of loop [14:1]:
V
V1


### Specialization of cost equations min/3
* CE 6 is refined into CE [23]
* CE 7 is refined into CE [24]
* CE 9 is refined into CE [25]
* CE 8 is refined into CE [26]


### Cost equations --> "Loop" of min/3
* CEs [26] --> Loop 18
* CEs [23] --> Loop 19
* CEs [24,25] --> Loop 20

### Ranking functions of CR min(V,V1,Out)
* RF of phase [18]: [V,V1]

#### Partial ranking functions of CR min(V,V1,Out)
* Partial RF of phase [18]:
- RF of loop [18:1]:
V
V1


### Specialization of cost equations minus/3
* CE 16 is refined into CE [27]
* CE 14 is refined into CE [28]
* CE 15 is refined into CE [29]


### Cost equations --> "Loop" of minus/3
* CEs [29] --> Loop 21
* CEs [27] --> Loop 22
* CEs [28] --> Loop 23

### Ranking functions of CR minus(V,V1,Out)
* RF of phase [21]: [V,V1]

#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [21]:
- RF of loop [21:1]:
V
V1


### Specialization of cost equations gcd/3
* CE 18 is refined into CE [30]
* CE 17 is refined into CE [31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64]


### Cost equations --> "Loop" of gcd/3
* CEs [48] --> Loop 24
* CEs [56] --> Loop 25
* CEs [60] --> Loop 26
* CEs [52] --> Loop 27
* CEs [44] --> Loop 28
* CEs [47] --> Loop 29
* CEs [55] --> Loop 30
* CEs [59] --> Loop 31
* CEs [63] --> Loop 32
* CEs [51] --> Loop 33
* CEs [43] --> Loop 34
* CEs [42,46] --> Loop 35
* CEs [36,38,40,50,54,58,62,64] --> Loop 36
* CEs [34] --> Loop 37
* CEs [33] --> Loop 38
* CEs [32] --> Loop 39
* CEs [31,35,37,39,41,45,49,53,57,61] --> Loop 40
* CEs [30] --> Loop 41

### Ranking functions of CR gcd(V,V1,Out)
* RF of phase [24,25,26,27,28,36]: [V+V1-3]
* RF of phase [37,39]: [V+V1-1]

#### Partial ranking functions of CR gcd(V,V1,Out)
* Partial RF of phase [24,25,26,27,28,36]:
- RF of loop [24:1,26:1,28:1,36:1]:
V-1 depends on loops [25:1,27:1]
- RF of loop [25:1,26:1,27:1,36:1]:
V+V1-3
* Partial RF of phase [37,39]:
- RF of loop [37:1]:
V depends on loops [39:1]
- RF of loop [39:1]:
V+V1-1


### Specialization of cost equations start/2
* CE 2 is refined into CE [65,66]
* CE 3 is refined into CE [67,68,69,70,71,72]
* CE 4 is refined into CE [73,74,75]
* CE 5 is refined into CE [76]


### Cost equations --> "Loop" of start/2
* CEs [68,73] --> Loop 42
* CEs [65,66,67,69,70,71,72,74,75,76] --> Loop 43

### Ranking functions of CR start(V,V1)

#### Partial ranking functions of CR start(V,V1)


Computing Bounds
=====================================

#### Cost of chains of max(V,V1,Out):
* Chain [[14],17]: 1*it(14)+1
Such that:it(14) =< V

with precondition: [V1=Out,V>=1,V1>=V]

* Chain [[14],16]: 1*it(14)+1
Such that:it(14) =< V1

with precondition: [V=Out,V1>=1,V>=V1]

* Chain [[14],15]: 1*it(14)+0
Such that:it(14) =< Out

with precondition: [Out>=1,V>=Out,V1>=Out]

* Chain [17]: 1
with precondition: [V=0,V1=Out,V1>=0]

* Chain [16]: 1
with precondition: [V1=0,V=Out,V>=0]

* Chain [15]: 0
with precondition: [Out=0,V>=0,V1>=0]


#### Cost of chains of min(V,V1,Out):
* Chain [[18],20]: 1*it(18)+1
Such that:it(18) =< Out

with precondition: [Out>=1,V>=Out,V1>=Out]

* Chain [[18],19]: 1*it(18)+1
Such that:it(18) =< Out

with precondition: [V1=Out,V1>=1,V>=V1]

* Chain [20]: 1
with precondition: [Out=0,V>=0,V1>=0]

* Chain [19]: 1
with precondition: [V1=0,Out=0,V>=0]


#### Cost of chains of minus(V,V1,Out):
* Chain [[21],23]: 1*it(21)+1
Such that:it(21) =< V1

with precondition: [V=Out+V1,V1>=1,V>=V1]

* Chain [[21],22]: 1*it(21)+0
Such that:it(21) =< V1

with precondition: [Out=0,V>=1,V1>=1]

* Chain [23]: 1
with precondition: [V1=0,V=Out,V>=0]

* Chain [22]: 0
with precondition: [Out=0,V>=0,V1>=0]


#### Cost of chains of gcd(V,V1,Out):
* Chain [[37,39],41]: 5*it(37)+6*it(39)+1*s(8)+0
Such that:aux(13) =< V
aux(14) =< V+V1
aux(15) =< V1
aux(6) =< aux(14)
it(37) =< aux(14)
it(39) =< aux(14)
aux(6) =< aux(15)+aux(13)
it(37) =< aux(15)+aux(13)
s(8) =< aux(6)

with precondition: [Out=0,V>=1,V1>=1]

* Chain [[37,39],40,41]: 5*it(37)+15*it(39)+1*s(8)+15*s(10)+4
Such that:aux(23) =< 1
aux(24) =< V
aux(25) =< V+V1
aux(26) =< V1
s(10) =< aux(23)
it(39) =< aux(25)
aux(6) =< aux(25)
it(37) =< aux(25)
aux(6) =< aux(26)+aux(24)
it(37) =< aux(26)+aux(24)
s(8) =< aux(6)

with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]

* Chain [[37,39],38,41]: 5*it(37)+6*it(39)+1*s(8)+1*s(34)+4
Such that:s(34) =< 1
aux(27) =< V
aux(28) =< V+V1
aux(29) =< V1
aux(6) =< aux(28)
it(37) =< aux(28)
it(39) =< aux(28)
aux(6) =< aux(29)+aux(27)
it(37) =< aux(29)+aux(27)
s(8) =< aux(6)

with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]

* Chain [[24,25,26,27,28,36],[37,39],41]: 18*it(24)+20*it(25)+5*it(37)+1*s(8)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+0
Such that:aux(90) =< V
aux(91) =< V+V1
aux(92) =< V1
aux(6) =< aux(91)
it(37) =< aux(91)
it(25) =< aux(91)
aux(6) =< aux(91)+aux(91)
it(37) =< aux(91)+aux(91)
s(8) =< aux(6)
aux(61) =< aux(91)
it(24) =< aux(91)
aux(55) =< aux(91)
aux(52) =< aux(92)
aux(62) =< aux(91)-1
aux(61) =< aux(92)+aux(92)+aux(90)
it(24) =< aux(92)+aux(92)+aux(90)
s(133) =< it(25)*aux(91)
s(132) =< aux(92)+aux(92)+aux(90)
s(155) =< aux(92)+aux(92)+aux(90)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(92)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[24,25,26,27,28,36],[37,39],40,41]: 18*it(24)+29*it(25)+5*it(37)+1*s(8)+15*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4
Such that:aux(23) =< 1
aux(93) =< V
aux(94) =< V+V1
aux(95) =< V1
s(10) =< aux(23)
it(25) =< aux(94)
aux(6) =< aux(94)
it(37) =< aux(94)
aux(6) =< aux(94)+aux(94)
it(37) =< aux(94)+aux(94)
s(8) =< aux(6)
aux(61) =< aux(94)
it(24) =< aux(94)
aux(55) =< aux(94)
aux(52) =< aux(95)
aux(62) =< aux(94)-1
aux(61) =< aux(95)+aux(95)+aux(93)
it(24) =< aux(95)+aux(95)+aux(93)
s(133) =< it(25)*aux(94)
s(132) =< aux(95)+aux(95)+aux(93)
s(155) =< aux(95)+aux(95)+aux(93)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(95)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[24,25,26,27,28,36],[37,39],38,41]: 18*it(24)+20*it(25)+5*it(37)+1*s(8)+1*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4
Such that:s(34) =< 1
aux(96) =< V
aux(97) =< V+V1
aux(98) =< V1
aux(6) =< aux(97)
it(37) =< aux(97)
it(25) =< aux(97)
aux(6) =< aux(97)+aux(97)
it(37) =< aux(97)+aux(97)
s(8) =< aux(6)
aux(61) =< aux(97)
it(24) =< aux(97)
aux(55) =< aux(97)
aux(52) =< aux(98)
aux(62) =< aux(97)-1
aux(61) =< aux(98)+aux(98)+aux(96)
it(24) =< aux(98)+aux(98)+aux(96)
s(133) =< it(25)*aux(97)
s(132) =< aux(98)+aux(98)+aux(96)
s(155) =< aux(98)+aux(98)+aux(96)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(98)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[24,25,26,27,28,36],41]: 18*it(24)+14*it(25)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+0
Such that:aux(99) =< V
aux(100) =< V+V1
aux(101) =< V1
aux(61) =< aux(100)
it(24) =< aux(100)
it(25) =< aux(100)
aux(55) =< aux(100)
aux(52) =< aux(101)
aux(62) =< aux(100)-1
aux(61) =< aux(101)+aux(101)+aux(99)
it(24) =< aux(101)+aux(101)+aux(99)
s(133) =< it(25)*aux(100)
s(132) =< aux(101)+aux(101)+aux(99)
s(155) =< aux(101)+aux(101)+aux(99)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(101)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[24,25,26,27,28,36],40,41]: 18*it(24)+32*it(25)+6*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4
Such that:aux(20) =< 1
aux(102) =< V
aux(103) =< V+V1
aux(104) =< V1
s(10) =< aux(20)
it(25) =< aux(103)
aux(61) =< aux(103)
it(24) =< aux(103)
aux(55) =< aux(103)
aux(52) =< aux(104)
aux(62) =< aux(103)-1
aux(61) =< aux(104)+aux(104)+aux(102)
it(24) =< aux(104)+aux(104)+aux(102)
s(133) =< it(25)*aux(103)
s(132) =< aux(104)+aux(104)+aux(102)
s(155) =< aux(104)+aux(104)+aux(102)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(104)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[24,25,26,27,28,36],35,41]: 18*it(24)+14*it(25)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9*s(160)+1*s(161)+4
Such that:s(161) =< 1
aux(109) =< V
aux(110) =< V+V1
aux(111) =< V1
s(160) =< aux(111)
aux(61) =< aux(110)
it(24) =< aux(110)
it(25) =< aux(110)
aux(55) =< aux(110)
aux(52) =< aux(111)
aux(62) =< aux(110)-1
aux(61) =< aux(111)+aux(111)+aux(109)
it(24) =< aux(111)+aux(111)+aux(109)
s(133) =< it(25)*aux(110)
s(132) =< aux(111)+aux(111)+aux(109)
s(155) =< aux(111)+aux(111)+aux(109)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(111)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],34,[37,39],41]: 18*it(24)+21*it(25)+5*it(37)+1*s(8)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(171)+5
Such that:aux(112) =< 1
aux(114) =< V
aux(115) =< V+V1
aux(116) =< V1
it(25) =< aux(115)
s(171) =< aux(112)
aux(6) =< aux(115)
it(37) =< aux(115)
aux(6) =< aux(112)+aux(115)
it(37) =< aux(112)+aux(115)
s(8) =< aux(6)
aux(61) =< aux(115)
it(24) =< aux(115)
aux(55) =< aux(115)
aux(52) =< aux(116)
aux(62) =< aux(115)-1
aux(61) =< aux(116)+aux(116)+aux(114)
it(24) =< aux(116)+aux(116)+aux(114)
s(133) =< it(25)*aux(115)
s(132) =< aux(116)+aux(116)+aux(114)
s(155) =< aux(116)+aux(116)+aux(114)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(116)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],34,[37,39],40,41]: 18*it(24)+30*it(25)+5*it(37)+1*s(8)+16*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(117) =< 1
aux(119) =< V
aux(120) =< V+V1
aux(121) =< V1
it(25) =< aux(120)
s(10) =< aux(117)
aux(6) =< aux(120)
it(37) =< aux(120)
aux(6) =< aux(117)+aux(120)
it(37) =< aux(117)+aux(120)
s(8) =< aux(6)
aux(61) =< aux(120)
it(24) =< aux(120)
aux(55) =< aux(120)
aux(52) =< aux(121)
aux(62) =< aux(120)-1
aux(61) =< aux(121)+aux(121)+aux(119)
it(24) =< aux(121)+aux(121)+aux(119)
s(133) =< it(25)*aux(120)
s(132) =< aux(121)+aux(121)+aux(119)
s(155) =< aux(121)+aux(121)+aux(119)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(121)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [[24,25,26,27,28,36],34,[37,39],38,41]: 18*it(24)+21*it(25)+5*it(37)+1*s(8)+2*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(122) =< 1
aux(124) =< V
aux(125) =< V+V1
aux(126) =< V1
it(25) =< aux(125)
s(34) =< aux(122)
aux(6) =< aux(125)
it(37) =< aux(125)
aux(6) =< aux(122)+aux(125)
it(37) =< aux(122)+aux(125)
s(8) =< aux(6)
aux(61) =< aux(125)
it(24) =< aux(125)
aux(55) =< aux(125)
aux(52) =< aux(126)
aux(62) =< aux(125)-1
aux(61) =< aux(126)+aux(126)+aux(124)
it(24) =< aux(126)+aux(126)+aux(124)
s(133) =< it(25)*aux(125)
s(132) =< aux(126)+aux(126)+aux(124)
s(155) =< aux(126)+aux(126)+aux(124)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(126)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [[24,25,26,27,28,36],34,41]: 18*it(24)+14*it(25)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(170)+1*s(171)+5
Such that:s(171) =< 1
aux(127) =< V
aux(128) =< V+V1
aux(129) =< V1
s(170) =< aux(129)
aux(61) =< aux(128)
it(24) =< aux(128)
it(25) =< aux(128)
aux(55) =< aux(128)
aux(52) =< aux(129)
aux(62) =< aux(128)-1
aux(61) =< aux(129)+aux(129)+aux(127)
it(24) =< aux(129)+aux(129)+aux(127)
s(133) =< it(25)*aux(128)
s(132) =< aux(129)+aux(129)+aux(127)
s(155) =< aux(129)+aux(129)+aux(127)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(129)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],34,40,41]: 18*it(24)+24*it(25)+16*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(130) =< 1
aux(131) =< V
aux(132) =< V+V1
aux(133) =< V1
it(25) =< aux(132)
s(10) =< aux(130)
aux(61) =< aux(132)
it(24) =< aux(132)
aux(55) =< aux(132)
aux(52) =< aux(133)
aux(62) =< aux(132)-1
aux(61) =< aux(133)+aux(133)+aux(131)
it(24) =< aux(133)+aux(133)+aux(131)
s(133) =< it(25)*aux(132)
s(132) =< aux(133)+aux(133)+aux(131)
s(155) =< aux(133)+aux(133)+aux(131)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(133)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],34,38,41]: 18*it(24)+14*it(25)+2*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(170)+9
Such that:aux(134) =< 1
aux(135) =< V
aux(136) =< V+V1
aux(137) =< V1
s(170) =< aux(137)
s(34) =< aux(134)
aux(61) =< aux(136)
it(24) =< aux(136)
it(25) =< aux(136)
aux(55) =< aux(136)
aux(52) =< aux(137)
aux(62) =< aux(136)-1
aux(61) =< aux(137)+aux(137)+aux(135)
it(24) =< aux(137)+aux(137)+aux(135)
s(133) =< it(25)*aux(136)
s(132) =< aux(137)+aux(137)+aux(135)
s(155) =< aux(137)+aux(137)+aux(135)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(137)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],33,[37,39],41]: 18*it(24)+21*it(25)+5*it(37)+1*s(8)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(173)+5
Such that:aux(138) =< 1
aux(140) =< V
aux(141) =< V+V1
aux(142) =< V1
it(25) =< aux(141)
s(173) =< aux(138)
aux(6) =< aux(141)
it(37) =< aux(141)
aux(6) =< aux(138)+aux(141)
it(37) =< aux(138)+aux(141)
s(8) =< aux(6)
aux(61) =< aux(141)
it(24) =< aux(141)
aux(55) =< aux(141)
aux(52) =< aux(142)
aux(62) =< aux(141)-1
aux(61) =< aux(142)+aux(142)+aux(140)
it(24) =< aux(142)+aux(142)+aux(140)
s(133) =< it(25)*aux(141)
s(132) =< aux(142)+aux(142)+aux(140)
s(155) =< aux(142)+aux(142)+aux(140)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(142)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],33,[37,39],40,41]: 18*it(24)+30*it(25)+5*it(37)+1*s(8)+16*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(143) =< 1
aux(145) =< V
aux(146) =< V+V1
aux(147) =< V1
it(25) =< aux(146)
s(10) =< aux(143)
aux(6) =< aux(146)
it(37) =< aux(146)
aux(6) =< aux(143)+aux(146)
it(37) =< aux(143)+aux(146)
s(8) =< aux(6)
aux(61) =< aux(146)
it(24) =< aux(146)
aux(55) =< aux(146)
aux(52) =< aux(147)
aux(62) =< aux(146)-1
aux(61) =< aux(147)+aux(147)+aux(145)
it(24) =< aux(147)+aux(147)+aux(145)
s(133) =< it(25)*aux(146)
s(132) =< aux(147)+aux(147)+aux(145)
s(155) =< aux(147)+aux(147)+aux(145)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(147)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[24,25,26,27,28,36],33,[37,39],38,41]: 18*it(24)+21*it(25)+5*it(37)+1*s(8)+2*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(148) =< 1
aux(150) =< V
aux(151) =< V+V1
aux(152) =< V1
it(25) =< aux(151)
s(34) =< aux(148)
aux(6) =< aux(151)
it(37) =< aux(151)
aux(6) =< aux(148)+aux(151)
it(37) =< aux(148)+aux(151)
s(8) =< aux(6)
aux(61) =< aux(151)
it(24) =< aux(151)
aux(55) =< aux(151)
aux(52) =< aux(152)
aux(62) =< aux(151)-1
aux(61) =< aux(152)+aux(152)+aux(150)
it(24) =< aux(152)+aux(152)+aux(150)
s(133) =< it(25)*aux(151)
s(132) =< aux(152)+aux(152)+aux(150)
s(155) =< aux(152)+aux(152)+aux(150)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(152)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[24,25,26,27,28,36],33,41]: 18*it(24)+14*it(25)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(172)+1*s(173)+5
Such that:s(173) =< 1
aux(153) =< V
aux(154) =< V+V1
aux(155) =< V1
s(172) =< aux(153)
aux(61) =< aux(154)
it(24) =< aux(154)
it(25) =< aux(154)
aux(55) =< aux(154)
aux(52) =< aux(155)
aux(62) =< aux(154)-1
aux(61) =< aux(155)+aux(155)+aux(153)
it(24) =< aux(155)+aux(155)+aux(153)
s(133) =< it(25)*aux(154)
s(132) =< aux(155)+aux(155)+aux(153)
s(155) =< aux(155)+aux(155)+aux(153)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(155)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],33,40,41]: 18*it(24)+24*it(25)+16*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(156) =< 1
aux(157) =< V
aux(158) =< V+V1
aux(159) =< V1
it(25) =< aux(158)
s(10) =< aux(156)
aux(61) =< aux(158)
it(24) =< aux(158)
aux(55) =< aux(158)
aux(52) =< aux(159)
aux(62) =< aux(158)-1
aux(61) =< aux(159)+aux(159)+aux(157)
it(24) =< aux(159)+aux(159)+aux(157)
s(133) =< it(25)*aux(158)
s(132) =< aux(159)+aux(159)+aux(157)
s(155) =< aux(159)+aux(159)+aux(157)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(159)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],33,38,41]: 18*it(24)+14*it(25)+2*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(172)+9
Such that:aux(160) =< 1
aux(161) =< V
aux(162) =< V+V1
aux(163) =< V1
s(172) =< aux(161)
s(34) =< aux(160)
aux(61) =< aux(162)
it(24) =< aux(162)
it(25) =< aux(162)
aux(55) =< aux(162)
aux(52) =< aux(163)
aux(62) =< aux(162)-1
aux(61) =< aux(163)+aux(163)+aux(161)
it(24) =< aux(163)+aux(163)+aux(161)
s(133) =< it(25)*aux(162)
s(132) =< aux(163)+aux(163)+aux(161)
s(155) =< aux(163)+aux(163)+aux(161)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(163)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],32,[37,39],41]: 18*it(24)+24*it(25)+5*it(37)+1*s(8)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4
Such that:aux(15) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(166) =< V
aux(167) =< V+V1
it(25) =< aux(167)
aux(6) =< aux(167)
it(37) =< aux(167)
aux(6) =< aux(15)+aux(167)
it(37) =< aux(15)+aux(167)
s(8) =< aux(6)
aux(61) =< aux(167)
it(24) =< aux(167)
aux(39) =< aux(88)
aux(39) =< aux(89)
aux(55) =< aux(167)
aux(52) =< aux(88)
aux(62) =< aux(167)-1
aux(61) =< aux(39)+aux(39)+aux(166)
it(24) =< aux(39)+aux(39)+aux(166)
s(133) =< it(25)*aux(167)
s(132) =< aux(39)+aux(39)+aux(166)
s(155) =< aux(39)+aux(39)+aux(166)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(88)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[24,25,26,27,28,36],32,[37,39],40,41]: 18*it(24)+33*it(25)+5*it(37)+1*s(8)+15*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+8
Such that:aux(168) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(170) =< V
aux(171) =< V+V1
it(25) =< aux(171)
s(10) =< aux(168)
aux(6) =< aux(171)
it(37) =< aux(171)
aux(6) =< aux(168)+aux(171)
it(37) =< aux(168)+aux(171)
s(8) =< aux(6)
aux(61) =< aux(171)
it(24) =< aux(171)
aux(39) =< aux(88)
aux(39) =< aux(89)
aux(55) =< aux(171)
aux(52) =< aux(88)
aux(62) =< aux(171)-1
aux(61) =< aux(39)+aux(39)+aux(170)
it(24) =< aux(39)+aux(39)+aux(170)
s(133) =< it(25)*aux(171)
s(132) =< aux(39)+aux(39)+aux(170)
s(155) =< aux(39)+aux(39)+aux(170)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(88)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=4,V1>=4,V+V1>=9]

* Chain [[24,25,26,27,28,36],32,[37,39],38,41]: 18*it(24)+24*it(25)+5*it(37)+1*s(8)+1*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+8
Such that:aux(172) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(174) =< V
aux(175) =< V+V1
s(34) =< aux(172)
it(25) =< aux(175)
aux(6) =< aux(175)
it(37) =< aux(175)
aux(6) =< aux(172)+aux(175)
it(37) =< aux(172)+aux(175)
s(8) =< aux(6)
aux(61) =< aux(175)
it(24) =< aux(175)
aux(39) =< aux(88)
aux(39) =< aux(89)
aux(55) =< aux(175)
aux(52) =< aux(88)
aux(62) =< aux(175)-1
aux(61) =< aux(39)+aux(39)+aux(174)
it(24) =< aux(39)+aux(39)+aux(174)
s(133) =< it(25)*aux(175)
s(132) =< aux(39)+aux(39)+aux(174)
s(155) =< aux(39)+aux(39)+aux(174)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(88)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=4,V1>=4,V+V1>=9]

* Chain [[24,25,26,27,28,36],32,41]: 18*it(24)+14*it(25)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4*s(174)+4
Such that:aux(177) =< V
aux(178) =< V+V1
aux(179) =< V1
s(174) =< aux(179)
aux(61) =< aux(178)
it(24) =< aux(178)
it(25) =< aux(178)
aux(55) =< aux(178)
aux(52) =< aux(179)
aux(62) =< aux(178)-1
aux(61) =< aux(179)+aux(179)+aux(177)
it(24) =< aux(179)+aux(179)+aux(177)
s(133) =< it(25)*aux(178)
s(132) =< aux(179)+aux(179)+aux(177)
s(155) =< aux(179)+aux(179)+aux(177)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(179)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],32,40,41]: 18*it(24)+14*it(25)+15*s(10)+13*s(22)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+8
Such that:aux(180) =< 1
aux(182) =< V
aux(183) =< V+V1
aux(184) =< V1
s(22) =< aux(184)
s(10) =< aux(180)
aux(61) =< aux(183)
it(24) =< aux(183)
it(25) =< aux(183)
aux(55) =< aux(183)
aux(52) =< aux(184)
aux(62) =< aux(183)-1
aux(61) =< aux(184)+aux(184)+aux(182)
it(24) =< aux(184)+aux(184)+aux(182)
s(133) =< it(25)*aux(183)
s(132) =< aux(184)+aux(184)+aux(182)
s(155) =< aux(184)+aux(184)+aux(182)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(184)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[24,25,26,27,28,36],32,38,41]: 18*it(24)+14*it(25)+1*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4*s(174)+8
Such that:s(34) =< 1
aux(186) =< V
aux(187) =< V+V1
aux(188) =< V1
s(174) =< aux(188)
aux(61) =< aux(187)
it(24) =< aux(187)
it(25) =< aux(187)
aux(55) =< aux(187)
aux(52) =< aux(188)
aux(62) =< aux(187)-1
aux(61) =< aux(188)+aux(188)+aux(186)
it(24) =< aux(188)+aux(188)+aux(186)
s(133) =< it(25)*aux(187)
s(132) =< aux(188)+aux(188)+aux(186)
s(155) =< aux(188)+aux(188)+aux(186)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(188)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[24,25,26,27,28,36],31,[37,39],41]: 18*it(24)+21*it(25)+5*it(37)+1*s(8)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(179)+4
Such that:aux(189) =< 1
aux(191) =< V
aux(192) =< V+V1
aux(193) =< V1
s(179) =< aux(189)
it(25) =< aux(192)
aux(6) =< aux(192)
it(37) =< aux(192)
aux(6) =< aux(189)+aux(192)
it(37) =< aux(189)+aux(192)
s(8) =< aux(6)
aux(61) =< aux(192)
it(24) =< aux(192)
aux(55) =< aux(192)
aux(52) =< aux(193)
aux(62) =< aux(192)-1
aux(61) =< aux(193)+aux(193)+aux(191)
it(24) =< aux(193)+aux(193)+aux(191)
s(133) =< it(25)*aux(192)
s(132) =< aux(193)+aux(193)+aux(191)
s(155) =< aux(193)+aux(193)+aux(191)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(193)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],31,[37,39],40,41]: 18*it(24)+30*it(25)+5*it(37)+1*s(8)+16*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+8
Such that:aux(194) =< 1
aux(196) =< V
aux(197) =< V+V1
aux(198) =< V1
s(10) =< aux(194)
it(25) =< aux(197)
aux(6) =< aux(197)
it(37) =< aux(197)
aux(6) =< aux(194)+aux(197)
it(37) =< aux(194)+aux(197)
s(8) =< aux(6)
aux(61) =< aux(197)
it(24) =< aux(197)
aux(55) =< aux(197)
aux(52) =< aux(198)
aux(62) =< aux(197)-1
aux(61) =< aux(198)+aux(198)+aux(196)
it(24) =< aux(198)+aux(198)+aux(196)
s(133) =< it(25)*aux(197)
s(132) =< aux(198)+aux(198)+aux(196)
s(155) =< aux(198)+aux(198)+aux(196)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(198)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[24,25,26,27,28,36],31,[37,39],38,41]: 18*it(24)+21*it(25)+5*it(37)+1*s(8)+2*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+8
Such that:aux(199) =< 1
aux(201) =< V
aux(202) =< V+V1
aux(203) =< V1
s(34) =< aux(199)
it(25) =< aux(202)
aux(6) =< aux(202)
it(37) =< aux(202)
aux(6) =< aux(199)+aux(202)
it(37) =< aux(199)+aux(202)
s(8) =< aux(6)
aux(61) =< aux(202)
it(24) =< aux(202)
aux(55) =< aux(202)
aux(52) =< aux(203)
aux(62) =< aux(202)-1
aux(61) =< aux(203)+aux(203)+aux(201)
it(24) =< aux(203)+aux(203)+aux(201)
s(133) =< it(25)*aux(202)
s(132) =< aux(203)+aux(203)+aux(201)
s(155) =< aux(203)+aux(203)+aux(201)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(203)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[24,25,26,27,28,36],31,41]: 18*it(24)+14*it(25)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(178)+1*s(179)+4
Such that:s(179) =< 1
aux(204) =< V
aux(205) =< V+V1
aux(206) =< V1
s(178) =< aux(206)
aux(61) =< aux(205)
it(24) =< aux(205)
it(25) =< aux(205)
aux(55) =< aux(205)
aux(52) =< aux(206)
aux(62) =< aux(205)-1
aux(61) =< aux(206)+aux(206)+aux(204)
it(24) =< aux(206)+aux(206)+aux(204)
s(133) =< it(25)*aux(205)
s(132) =< aux(206)+aux(206)+aux(204)
s(155) =< aux(206)+aux(206)+aux(204)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(206)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],31,40,41]: 18*it(24)+24*it(25)+16*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+8
Such that:aux(207) =< 1
aux(209) =< V
aux(210) =< V+V1
aux(211) =< V1
s(10) =< aux(207)
it(25) =< aux(210)
aux(61) =< aux(210)
it(24) =< aux(210)
aux(55) =< aux(210)
aux(52) =< aux(211)
aux(62) =< aux(210)-1
aux(61) =< aux(211)+aux(211)+aux(209)
it(24) =< aux(211)+aux(211)+aux(209)
s(133) =< it(25)*aux(210)
s(132) =< aux(211)+aux(211)+aux(209)
s(155) =< aux(211)+aux(211)+aux(209)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(211)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],31,38,41]: 18*it(24)+14*it(25)+2*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+1*s(178)+8
Such that:aux(212) =< 1
aux(213) =< V
aux(214) =< V+V1
aux(215) =< V1
s(178) =< aux(215)
s(34) =< aux(212)
aux(61) =< aux(214)
it(24) =< aux(214)
it(25) =< aux(214)
aux(55) =< aux(214)
aux(52) =< aux(215)
aux(62) =< aux(214)-1
aux(61) =< aux(215)+aux(215)+aux(213)
it(24) =< aux(215)+aux(215)+aux(213)
s(133) =< it(25)*aux(214)
s(132) =< aux(215)+aux(215)+aux(213)
s(155) =< aux(215)+aux(215)+aux(213)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(215)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],30,[37,39],41]: 18*it(24)+10*it(25)+5*it(37)+10*it(39)+1*s(8)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(134)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+5
Such that:aux(15) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(218) =< V
aux(219) =< V+V1
aux(220) =< V+V1+1
it(39) =< aux(220)
aux(6) =< aux(220)
it(37) =< aux(220)
aux(6) =< aux(15)+aux(219)
it(37) =< aux(15)+aux(219)
s(8) =< aux(6)
aux(61) =< aux(219)
aux(64) =< aux(219)
it(24) =< aux(219)
it(25) =< aux(219)
aux(61) =< aux(220)
aux(64) =< aux(220)
it(24) =< aux(220)
it(25) =< aux(220)
aux(39) =< aux(88)
aux(39) =< aux(89)
aux(55) =< aux(219)
aux(52) =< aux(88)
aux(62) =< aux(219)-1
aux(61) =< aux(39)+aux(39)+aux(218)
it(24) =< aux(39)+aux(39)+aux(218)
s(134) =< aux(64)
s(133) =< it(25)*aux(219)
s(132) =< aux(39)+aux(39)+aux(218)
s(155) =< aux(39)+aux(39)+aux(218)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(88)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[24,25,26,27,28,36],30,[37,39],40,41]: 18*it(24)+10*it(25)+5*it(37)+19*it(39)+1*s(8)+15*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(134)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(221) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(223) =< V
aux(224) =< V+V1
aux(225) =< V+V1+1
it(39) =< aux(225)
s(10) =< aux(221)
aux(6) =< aux(225)
it(37) =< aux(225)
aux(6) =< aux(221)+aux(224)
it(37) =< aux(221)+aux(224)
s(8) =< aux(6)
aux(61) =< aux(224)
aux(64) =< aux(224)
it(24) =< aux(224)
it(25) =< aux(224)
aux(61) =< aux(225)
aux(64) =< aux(225)
it(24) =< aux(225)
it(25) =< aux(225)
aux(39) =< aux(88)
aux(39) =< aux(89)
aux(55) =< aux(224)
aux(52) =< aux(88)
aux(62) =< aux(224)-1
aux(61) =< aux(39)+aux(39)+aux(223)
it(24) =< aux(39)+aux(39)+aux(223)
s(134) =< aux(64)
s(133) =< it(25)*aux(224)
s(132) =< aux(39)+aux(39)+aux(223)
s(155) =< aux(39)+aux(39)+aux(223)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(88)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=4,V1>=4]

* Chain [[24,25,26,27,28,36],30,[37,39],38,41]: 18*it(24)+10*it(25)+5*it(37)+10*it(39)+1*s(8)+1*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(134)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(226) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(228) =< V
aux(229) =< V+V1
aux(230) =< V+V1+1
it(39) =< aux(230)
s(34) =< aux(226)
aux(6) =< aux(230)
it(37) =< aux(230)
aux(6) =< aux(226)+aux(229)
it(37) =< aux(226)+aux(229)
s(8) =< aux(6)
aux(61) =< aux(229)
aux(64) =< aux(229)
it(24) =< aux(229)
it(25) =< aux(229)
aux(61) =< aux(230)
aux(64) =< aux(230)
it(24) =< aux(230)
it(25) =< aux(230)
aux(39) =< aux(88)
aux(39) =< aux(89)
aux(55) =< aux(229)
aux(52) =< aux(88)
aux(62) =< aux(229)-1
aux(61) =< aux(39)+aux(39)+aux(228)
it(24) =< aux(39)+aux(39)+aux(228)
s(134) =< aux(64)
s(133) =< it(25)*aux(229)
s(132) =< aux(39)+aux(39)+aux(228)
s(155) =< aux(39)+aux(39)+aux(228)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(88)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=4,V1>=4]

* Chain [[24,25,26,27,28,36],30,41]: 18*it(24)+14*it(25)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4*s(180)+5
Such that:aux(232) =< V
aux(233) =< V+V1
aux(234) =< V1
s(180) =< aux(232)
aux(61) =< aux(233)
it(24) =< aux(233)
it(25) =< aux(233)
aux(55) =< aux(233)
aux(52) =< aux(234)
aux(62) =< aux(233)-1
aux(61) =< aux(234)+aux(234)+aux(232)
it(24) =< aux(234)+aux(234)+aux(232)
s(133) =< it(25)*aux(233)
s(132) =< aux(234)+aux(234)+aux(232)
s(155) =< aux(234)+aux(234)+aux(232)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(234)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],30,40,41]: 18*it(24)+27*it(25)+15*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(235) =< 1
aux(237) =< V
aux(238) =< V+V1
aux(239) =< V1
it(25) =< aux(238)
s(10) =< aux(235)
aux(61) =< aux(238)
it(24) =< aux(238)
aux(55) =< aux(238)
aux(52) =< aux(239)
aux(62) =< aux(238)-1
aux(61) =< aux(239)+aux(239)+aux(237)
it(24) =< aux(239)+aux(239)+aux(237)
s(133) =< it(25)*aux(238)
s(132) =< aux(239)+aux(239)+aux(237)
s(155) =< aux(239)+aux(239)+aux(237)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(239)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[24,25,26,27,28,36],30,38,41]: 18*it(24)+14*it(25)+1*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4*s(180)+9
Such that:s(34) =< 1
aux(241) =< V
aux(242) =< V+V1
aux(243) =< V1
s(180) =< aux(241)
aux(61) =< aux(242)
it(24) =< aux(242)
it(25) =< aux(242)
aux(55) =< aux(242)
aux(52) =< aux(243)
aux(62) =< aux(242)-1
aux(61) =< aux(243)+aux(243)+aux(241)
it(24) =< aux(243)+aux(243)+aux(241)
s(133) =< it(25)*aux(242)
s(132) =< aux(243)+aux(243)+aux(241)
s(155) =< aux(243)+aux(243)+aux(241)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(243)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[24,25,26,27,28,36],29,[37,39],41]: 18*it(24)+10*it(25)+5*it(37)+10*it(39)+1*s(8)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(134)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+5
Such that:aux(15) =< 1
aux(246) =< V
aux(247) =< V+V1
aux(248) =< V+V1+1
aux(249) =< V1
it(39) =< aux(248)
aux(6) =< aux(248)
it(37) =< aux(248)
aux(6) =< aux(15)+aux(247)
it(37) =< aux(15)+aux(247)
s(8) =< aux(6)
aux(61) =< aux(247)
aux(64) =< aux(247)
it(24) =< aux(247)
it(25) =< aux(247)
aux(61) =< aux(248)
aux(64) =< aux(248)
it(24) =< aux(248)
it(25) =< aux(248)
aux(55) =< aux(247)
aux(52) =< aux(249)
aux(62) =< aux(247)-1
aux(61) =< aux(249)+aux(249)+aux(246)
it(24) =< aux(249)+aux(249)+aux(246)
s(134) =< aux(64)
s(133) =< it(25)*aux(247)
s(132) =< aux(249)+aux(249)+aux(246)
s(155) =< aux(249)+aux(249)+aux(246)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(249)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [[24,25,26,27,28,36],29,[37,39],40,41]: 18*it(24)+10*it(25)+5*it(37)+19*it(39)+1*s(8)+15*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(134)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(250) =< 1
aux(252) =< V
aux(253) =< V+V1
aux(254) =< V+V1+1
aux(255) =< V1
it(39) =< aux(254)
s(10) =< aux(250)
aux(6) =< aux(254)
it(37) =< aux(254)
aux(6) =< aux(250)+aux(253)
it(37) =< aux(250)+aux(253)
s(8) =< aux(6)
aux(61) =< aux(253)
aux(64) =< aux(253)
it(24) =< aux(253)
it(25) =< aux(253)
aux(61) =< aux(254)
aux(64) =< aux(254)
it(24) =< aux(254)
it(25) =< aux(254)
aux(55) =< aux(253)
aux(52) =< aux(255)
aux(62) =< aux(253)-1
aux(61) =< aux(255)+aux(255)+aux(252)
it(24) =< aux(255)+aux(255)+aux(252)
s(134) =< aux(64)
s(133) =< it(25)*aux(253)
s(132) =< aux(255)+aux(255)+aux(252)
s(155) =< aux(255)+aux(255)+aux(252)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(255)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=7]

* Chain [[24,25,26,27,28,36],29,[37,39],38,41]: 18*it(24)+10*it(25)+5*it(37)+10*it(39)+1*s(8)+1*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(134)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(256) =< 1
aux(258) =< V
aux(259) =< V+V1
aux(260) =< V+V1+1
aux(261) =< V1
it(39) =< aux(260)
s(34) =< aux(256)
aux(6) =< aux(260)
it(37) =< aux(260)
aux(6) =< aux(256)+aux(259)
it(37) =< aux(256)+aux(259)
s(8) =< aux(6)
aux(61) =< aux(259)
aux(64) =< aux(259)
it(24) =< aux(259)
it(25) =< aux(259)
aux(61) =< aux(260)
aux(64) =< aux(260)
it(24) =< aux(260)
it(25) =< aux(260)
aux(55) =< aux(259)
aux(52) =< aux(261)
aux(62) =< aux(259)-1
aux(61) =< aux(261)+aux(261)+aux(258)
it(24) =< aux(261)+aux(261)+aux(258)
s(134) =< aux(64)
s(133) =< it(25)*aux(259)
s(132) =< aux(261)+aux(261)+aux(258)
s(155) =< aux(261)+aux(261)+aux(258)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(261)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=7]

* Chain [[24,25,26,27,28,36],29,41]: 18*it(24)+14*it(25)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4*s(184)+5
Such that:aux(263) =< V
aux(264) =< V+V1
aux(265) =< V1
s(184) =< aux(265)
aux(61) =< aux(264)
it(24) =< aux(264)
it(25) =< aux(264)
aux(55) =< aux(264)
aux(52) =< aux(265)
aux(62) =< aux(264)-1
aux(61) =< aux(265)+aux(265)+aux(263)
it(24) =< aux(265)+aux(265)+aux(263)
s(133) =< it(25)*aux(264)
s(132) =< aux(265)+aux(265)+aux(263)
s(155) =< aux(265)+aux(265)+aux(263)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(265)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[24,25,26,27,28,36],29,40,41]: 18*it(24)+27*it(25)+15*s(10)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+9
Such that:aux(266) =< 1
aux(268) =< V
aux(269) =< V+V1
aux(270) =< V1
it(25) =< aux(269)
s(10) =< aux(266)
aux(61) =< aux(269)
it(24) =< aux(269)
aux(55) =< aux(269)
aux(52) =< aux(270)
aux(62) =< aux(269)-1
aux(61) =< aux(270)+aux(270)+aux(268)
it(24) =< aux(270)+aux(270)+aux(268)
s(133) =< it(25)*aux(269)
s(132) =< aux(270)+aux(270)+aux(268)
s(155) =< aux(270)+aux(270)+aux(268)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(270)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [[24,25,26,27,28,36],29,38,41]: 18*it(24)+14*it(25)+1*s(34)+2*s(128)+3*s(129)+8*s(130)+1*s(133)+4*s(135)+1*s(138)+6*s(139)+28*s(140)+1*s(142)+3*s(154)+4*s(184)+9
Such that:s(34) =< 1
aux(272) =< V
aux(273) =< V+V1
aux(274) =< V1
s(184) =< aux(274)
aux(61) =< aux(273)
it(24) =< aux(273)
it(25) =< aux(273)
aux(55) =< aux(273)
aux(52) =< aux(274)
aux(62) =< aux(273)-1
aux(61) =< aux(274)+aux(274)+aux(272)
it(24) =< aux(274)+aux(274)+aux(272)
s(133) =< it(25)*aux(273)
s(132) =< aux(274)+aux(274)+aux(272)
s(155) =< aux(274)+aux(274)+aux(272)
s(136) =< it(25)*aux(55)
s(142) =< it(25)*aux(55)
s(141) =< it(24)*aux(55)
s(131) =< it(24)*aux(52)
s(155) =< it(24)*aux(55)
s(128) =< it(24)*aux(52)
s(139) =< aux(61)
s(138) =< it(24)*aux(62)
s(132) =< it(24)*aux(274)
s(140) =< s(141)
s(130) =< s(131)
s(154) =< s(155)
s(135) =< s(136)
s(129) =< s(132)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [41]: 0
with precondition: [Out=0,V>=0,V1>=0]

* Chain [40,41]: 6*s(10)+9*s(14)+9*s(22)+4
Such that:aux(20) =< 1
aux(21) =< V
aux(22) =< V1
s(10) =< aux(20)
s(22) =< aux(21)
s(14) =< aux(22)

with precondition: [Out=0,V>=1,V1>=1]

* Chain [38,41]: 1*s(34)+4
Such that:s(34) =< 1

with precondition: [V1=1,Out=0,V>=1]

* Chain [35,41]: 9*s(160)+1*s(161)+4
Such that:s(161) =< 1
aux(108) =< V1
s(160) =< aux(108)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [34,[37,39],41]: 5*it(37)+6*it(39)+1*s(8)+1*s(170)+1*s(171)+5
Such that:s(170) =< V1
aux(112) =< 1
aux(113) =< V
s(171) =< aux(112)
aux(6) =< aux(113)
it(37) =< aux(113)
it(39) =< aux(113)
aux(6) =< aux(112)+aux(113)
it(37) =< aux(112)+aux(113)
s(8) =< aux(6)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [34,[37,39],40,41]: 5*it(37)+15*it(39)+1*s(8)+16*s(10)+1*s(170)+9
Such that:s(170) =< V1
aux(117) =< 1
aux(118) =< V
s(10) =< aux(117)
it(39) =< aux(118)
aux(6) =< aux(118)
it(37) =< aux(118)
aux(6) =< aux(117)+aux(118)
it(37) =< aux(117)+aux(118)
s(8) =< aux(6)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]

* Chain [34,[37,39],38,41]: 5*it(37)+6*it(39)+1*s(8)+2*s(34)+1*s(170)+9
Such that:s(170) =< V1
aux(122) =< 1
aux(123) =< V
s(34) =< aux(122)
aux(6) =< aux(123)
it(37) =< aux(123)
it(39) =< aux(123)
aux(6) =< aux(122)+aux(123)
it(37) =< aux(122)+aux(123)
s(8) =< aux(6)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]

* Chain [34,41]: 1*s(170)+1*s(171)+5
Such that:s(171) =< 1
s(170) =< V1

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [34,40,41]: 16*s(10)+9*s(22)+1*s(170)+9
Such that:aux(21) =< V
s(170) =< V1
aux(130) =< 1
s(10) =< aux(130)
s(22) =< aux(21)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [34,38,41]: 2*s(34)+1*s(170)+9
Such that:s(170) =< V1
aux(134) =< 1
s(34) =< aux(134)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [33,[37,39],41]: 5*it(37)+6*it(39)+1*s(8)+1*s(172)+1*s(173)+5
Such that:s(172) =< V
aux(138) =< 1
aux(139) =< V1
s(173) =< aux(138)
aux(6) =< aux(139)
it(37) =< aux(139)
it(39) =< aux(139)
aux(6) =< aux(138)+aux(139)
it(37) =< aux(138)+aux(139)
s(8) =< aux(6)

with precondition: [Out=0,V>=2,V1>=V]

* Chain [33,[37,39],40,41]: 5*it(37)+15*it(39)+1*s(8)+16*s(10)+1*s(172)+9
Such that:s(172) =< V
aux(143) =< 1
aux(144) =< V1
s(10) =< aux(143)
it(39) =< aux(144)
aux(6) =< aux(144)
it(37) =< aux(144)
aux(6) =< aux(143)+aux(144)
it(37) =< aux(143)+aux(144)
s(8) =< aux(6)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [33,[37,39],38,41]: 5*it(37)+6*it(39)+1*s(8)+2*s(34)+1*s(172)+9
Such that:s(172) =< V
aux(148) =< 1
aux(149) =< V1
s(34) =< aux(148)
aux(6) =< aux(149)
it(37) =< aux(149)
it(39) =< aux(149)
aux(6) =< aux(148)+aux(149)
it(37) =< aux(148)+aux(149)
s(8) =< aux(6)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [33,41]: 1*s(172)+1*s(173)+5
Such that:s(173) =< 1
s(172) =< V

with precondition: [Out=0,V>=2,V1>=V]

* Chain [33,40,41]: 16*s(10)+9*s(22)+1*s(172)+9
Such that:s(172) =< V
aux(21) =< V1
aux(156) =< 1
s(10) =< aux(156)
s(22) =< aux(21)

with precondition: [Out=0,V>=2,V1>=V]

* Chain [33,38,41]: 2*s(34)+1*s(172)+9
Such that:s(172) =< V
aux(160) =< 1
s(34) =< aux(160)

with precondition: [Out=0,V>=2,V1>=V]

* Chain [32,[37,39],41]: 5*it(37)+6*it(39)+1*s(8)+4*s(174)+4
Such that:aux(15) =< 1
aux(14) =< V1+1
aux(165) =< V1
s(174) =< aux(165)
aux(6) =< aux(14)
it(37) =< aux(14)
it(39) =< aux(14)
aux(6) =< aux(15)+aux(165)
it(37) =< aux(15)+aux(165)
s(8) =< aux(6)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [32,[37,39],40,41]: 5*it(37)+15*it(39)+1*s(8)+15*s(10)+4*s(174)+8
Such that:aux(25) =< V1+1
aux(168) =< 1
aux(169) =< V1
s(174) =< aux(169)
s(10) =< aux(168)
it(39) =< aux(25)
aux(6) =< aux(25)
it(37) =< aux(25)
aux(6) =< aux(168)+aux(169)
it(37) =< aux(168)+aux(169)
s(8) =< aux(6)

with precondition: [Out=0,V>=4,V1>=4]

* Chain [32,[37,39],38,41]: 5*it(37)+6*it(39)+1*s(8)+1*s(34)+4*s(174)+8
Such that:aux(28) =< V1+1
aux(172) =< 1
aux(173) =< V1
s(34) =< aux(172)
s(174) =< aux(173)
aux(6) =< aux(28)
it(37) =< aux(28)
it(39) =< aux(28)
aux(6) =< aux(172)+aux(173)
it(37) =< aux(172)+aux(173)
s(8) =< aux(6)

with precondition: [Out=0,V>=4,V1>=4]

* Chain [32,41]: 4*s(174)+4
Such that:aux(176) =< V1
s(174) =< aux(176)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [32,40,41]: 15*s(10)+13*s(22)+8
Such that:aux(180) =< 1
aux(181) =< V1
s(22) =< aux(181)
s(10) =< aux(180)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [32,38,41]: 1*s(34)+4*s(174)+8
Such that:s(34) =< 1
aux(185) =< V1
s(174) =< aux(185)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [31,[37,39],41]: 5*it(37)+7*it(39)+1*s(8)+1*s(179)+4
Such that:aux(189) =< 1
aux(190) =< V
s(179) =< aux(189)
it(39) =< aux(190)
aux(6) =< aux(190)
it(37) =< aux(190)
aux(6) =< aux(189)+aux(190)
it(37) =< aux(189)+aux(190)
s(8) =< aux(6)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [31,[37,39],40,41]: 5*it(37)+16*it(39)+1*s(8)+16*s(10)+8
Such that:aux(194) =< 1
aux(195) =< V
s(10) =< aux(194)
it(39) =< aux(195)
aux(6) =< aux(195)
it(37) =< aux(195)
aux(6) =< aux(194)+aux(195)
it(37) =< aux(194)+aux(195)
s(8) =< aux(6)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [31,[37,39],38,41]: 5*it(37)+7*it(39)+1*s(8)+2*s(34)+8
Such that:aux(199) =< 1
aux(200) =< V
s(34) =< aux(199)
it(39) =< aux(200)
aux(6) =< aux(200)
it(37) =< aux(200)
aux(6) =< aux(199)+aux(200)
it(37) =< aux(199)+aux(200)
s(8) =< aux(6)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [31,41]: 1*s(178)+1*s(179)+4
Such that:s(179) =< 1
s(178) =< V1

with precondition: [Out=0,V>=2,V1>=2]

* Chain [31,40,41]: 16*s(10)+10*s(22)+8
Such that:aux(207) =< 1
aux(208) =< V
s(10) =< aux(207)
s(22) =< aux(208)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [31,38,41]: 2*s(34)+1*s(178)+8
Such that:s(178) =< V1
aux(212) =< 1
s(34) =< aux(212)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [30,[37,39],41]: 5*it(37)+9*it(39)+1*s(8)+1*s(180)+5
Such that:aux(15) =< 1
s(180) =< V
aux(13) =< V1
aux(217) =< V1+1
aux(6) =< aux(217)
it(37) =< aux(217)
it(39) =< aux(217)
aux(6) =< aux(15)+aux(13)
it(37) =< aux(15)+aux(13)
s(8) =< aux(6)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [30,[37,39],40,41]: 5*it(37)+18*it(39)+1*s(8)+15*s(10)+1*s(180)+9
Such that:s(180) =< V
aux(24) =< V1
aux(221) =< 1
aux(222) =< V1+1
s(10) =< aux(221)
it(39) =< aux(222)
aux(6) =< aux(222)
it(37) =< aux(222)
aux(6) =< aux(221)+aux(24)
it(37) =< aux(221)+aux(24)
s(8) =< aux(6)

with precondition: [Out=0,V>=2,V1>=4,V1>=V]

* Chain [30,[37,39],38,41]: 5*it(37)+9*it(39)+1*s(8)+1*s(34)+1*s(180)+9
Such that:s(180) =< V
aux(27) =< V1
aux(226) =< 1
aux(227) =< V1+1
s(34) =< aux(226)
aux(6) =< aux(227)
it(37) =< aux(227)
it(39) =< aux(227)
aux(6) =< aux(226)+aux(27)
it(37) =< aux(226)+aux(27)
s(8) =< aux(6)

with precondition: [Out=0,V>=2,V1>=4,V1>=V]

* Chain [30,41]: 4*s(180)+5
Such that:aux(231) =< V
s(180) =< aux(231)

with precondition: [Out=0,V>=2,V1>=V]

* Chain [30,40,41]: 15*s(10)+12*s(22)+1*s(180)+9
Such that:s(180) =< V
aux(235) =< 1
aux(236) =< V1
s(10) =< aux(235)
s(22) =< aux(236)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [30,38,41]: 1*s(34)+4*s(180)+9
Such that:s(34) =< 1
aux(240) =< V
s(180) =< aux(240)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [29,[37,39],41]: 5*it(37)+9*it(39)+1*s(8)+1*s(184)+5
Such that:aux(15) =< 1
aux(13) =< V
s(184) =< V1
aux(245) =< V+1
aux(6) =< aux(245)
it(37) =< aux(245)
it(39) =< aux(245)
aux(6) =< aux(15)+aux(13)
it(37) =< aux(15)+aux(13)
s(8) =< aux(6)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]

* Chain [29,[37,39],40,41]: 5*it(37)+18*it(39)+1*s(8)+15*s(10)+1*s(184)+9
Such that:aux(24) =< V
s(184) =< V1
aux(250) =< 1
aux(251) =< V+1
s(10) =< aux(250)
it(39) =< aux(251)
aux(6) =< aux(251)
it(37) =< aux(251)
aux(6) =< aux(250)+aux(24)
it(37) =< aux(250)+aux(24)
s(8) =< aux(6)

with precondition: [Out=0,V>=4,V1>=2,V>=V1]

* Chain [29,[37,39],38,41]: 5*it(37)+9*it(39)+1*s(8)+1*s(34)+1*s(184)+9
Such that:aux(27) =< V
s(184) =< V1
aux(256) =< 1
aux(257) =< V+1
s(34) =< aux(256)
aux(6) =< aux(257)
it(37) =< aux(257)
it(39) =< aux(257)
aux(6) =< aux(256)+aux(27)
it(37) =< aux(256)+aux(27)
s(8) =< aux(6)

with precondition: [Out=0,V>=4,V1>=2,V>=V1]

* Chain [29,41]: 4*s(184)+5
Such that:aux(262) =< V1
s(184) =< aux(262)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [29,40,41]: 15*s(10)+12*s(22)+1*s(184)+9
Such that:s(184) =< V1
aux(266) =< 1
aux(267) =< V
s(10) =< aux(266)
s(22) =< aux(267)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]

* Chain [29,38,41]: 1*s(34)+4*s(184)+9
Such that:s(34) =< 1
aux(271) =< V1
s(184) =< aux(271)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]


#### Cost of chains of start(V,V1):
* Chain [43]: 167*s(1612)+126*s(1614)+467*s(1625)+15*s(1629)+36*s(1630)+3*s(1631)+30*s(1633)+63*s(1634)+6*s(1635)+30*s(1637)+6*s(1638)+594*s(1640)+761*s(1641)+36*s(1645)+36*s(1649)+66*s(1652)+198*s(1653)+33*s(1654)+924*s(1655)+264*s(1656)+99*s(1657)+144*s(1658)+99*s(1659)+78*s(1660)+30*s(1662)+6*s(1663)+54*s(1666)+60*s(1667)+24*s(1668)+6*s(1669)+6*s(1673)+6*s(1676)+18*s(1677)+3*s(1678)+84*s(1679)+24*s(1680)+9*s(1681)+24*s(1682)+9*s(1683)+54*s(1685)+6*s(1691)+18*s(1692)+3*s(1693)+84*s(1694)+24*s(1695)+9*s(1696)+9*s(1697)+60*s(1699)+12*s(1700)+54*s(1702)+6*s(1707)+18*s(1708)+3*s(1709)+84*s(1710)+24*s(1711)+9*s(1712)+9*s(1713)+15*s(1715)+3*s(1716)+15*s(1718)+3*s(1719)+15*s(1721)+3*s(1722)+9
Such that:s(1618) =< 1
s(1620) =< V+1
s(1621) =< V+V1
s(1622) =< V+V1+1
s(1624) =< V1+1
aux(282) =< V
aux(283) =< V1
s(1614) =< aux(282)
s(1612) =< aux(283)
s(1625) =< s(1618)
s(1628) =< s(1620)
s(1629) =< s(1620)
s(1630) =< s(1620)
s(1628) =< s(1618)+aux(282)
s(1629) =< s(1618)+aux(282)
s(1631) =< s(1628)
s(1632) =< s(1624)
s(1633) =< s(1624)
s(1634) =< s(1624)
s(1632) =< s(1618)+aux(283)
s(1633) =< s(1618)+aux(283)
s(1635) =< s(1632)
s(1636) =< aux(282)
s(1637) =< aux(282)
s(1636) =< s(1618)+aux(282)
s(1637) =< s(1618)+aux(282)
s(1638) =< s(1636)
s(1639) =< s(1621)
s(1640) =< s(1621)
s(1641) =< s(1621)
s(1642) =< s(1621)
s(1643) =< aux(283)
s(1644) =< s(1621)-1
s(1639) =< aux(283)+aux(283)+aux(282)
s(1640) =< aux(283)+aux(283)+aux(282)
s(1645) =< s(1641)*s(1621)
s(1646) =< aux(283)+aux(283)+aux(282)
s(1647) =< aux(283)+aux(283)+aux(282)
s(1648) =< s(1641)*s(1642)
s(1649) =< s(1641)*s(1642)
s(1650) =< s(1640)*s(1642)
s(1651) =< s(1640)*s(1643)
s(1647) =< s(1640)*s(1642)
s(1652) =< s(1640)*s(1643)
s(1653) =< s(1639)
s(1654) =< s(1640)*s(1644)
s(1646) =< s(1640)*aux(283)
s(1655) =< s(1650)
s(1656) =< s(1651)
s(1657) =< s(1647)
s(1658) =< s(1648)
s(1659) =< s(1646)
s(1660) =< s(1622)
s(1661) =< s(1622)
s(1662) =< s(1622)
s(1661) =< s(1618)+s(1621)
s(1662) =< s(1618)+s(1621)
s(1663) =< s(1661)
s(1664) =< s(1621)
s(1665) =< s(1621)
s(1666) =< s(1621)
s(1667) =< s(1621)
s(1664) =< s(1622)
s(1665) =< s(1622)
s(1666) =< s(1622)
s(1667) =< s(1622)
s(1664) =< aux(283)+aux(283)+aux(282)
s(1666) =< aux(283)+aux(283)+aux(282)
s(1668) =< s(1665)
s(1669) =< s(1667)*s(1621)
s(1670) =< aux(283)+aux(283)+aux(282)
s(1671) =< aux(283)+aux(283)+aux(282)
s(1672) =< s(1667)*s(1642)
s(1673) =< s(1667)*s(1642)
s(1674) =< s(1666)*s(1642)
s(1675) =< s(1666)*s(1643)
s(1671) =< s(1666)*s(1642)
s(1676) =< s(1666)*s(1643)
s(1677) =< s(1664)
s(1678) =< s(1666)*s(1644)
s(1670) =< s(1666)*aux(283)
s(1679) =< s(1674)
s(1680) =< s(1675)
s(1681) =< s(1671)
s(1682) =< s(1672)
s(1683) =< s(1670)
s(1684) =< s(1621)
s(1685) =< s(1621)
s(1684) =< s(1622)
s(1685) =< s(1622)
s(1686) =< aux(283)
s(1686) =< s(1624)
s(1684) =< s(1686)+s(1686)+aux(282)
s(1685) =< s(1686)+s(1686)+aux(282)
s(1687) =< s(1686)+s(1686)+aux(282)
s(1688) =< s(1686)+s(1686)+aux(282)
s(1689) =< s(1685)*s(1642)
s(1690) =< s(1685)*s(1643)
s(1688) =< s(1685)*s(1642)
s(1691) =< s(1685)*s(1643)
s(1692) =< s(1684)
s(1693) =< s(1685)*s(1644)
s(1687) =< s(1685)*aux(283)
s(1694) =< s(1689)
s(1695) =< s(1690)
s(1696) =< s(1688)
s(1697) =< s(1687)
s(1698) =< s(1621)
s(1699) =< s(1621)
s(1698) =< s(1618)+s(1621)
s(1699) =< s(1618)+s(1621)
s(1700) =< s(1698)
s(1701) =< s(1621)
s(1702) =< s(1621)
s(1701) =< s(1686)+s(1686)+aux(282)
s(1702) =< s(1686)+s(1686)+aux(282)
s(1703) =< s(1686)+s(1686)+aux(282)
s(1704) =< s(1686)+s(1686)+aux(282)
s(1705) =< s(1702)*s(1642)
s(1706) =< s(1702)*s(1643)
s(1704) =< s(1702)*s(1642)
s(1707) =< s(1702)*s(1643)
s(1708) =< s(1701)
s(1709) =< s(1702)*s(1644)
s(1703) =< s(1702)*aux(283)
s(1710) =< s(1705)
s(1711) =< s(1706)
s(1712) =< s(1704)
s(1713) =< s(1703)
s(1714) =< s(1621)
s(1715) =< s(1621)
s(1714) =< s(1621)+s(1621)
s(1715) =< s(1621)+s(1621)
s(1716) =< s(1714)
s(1717) =< s(1621)
s(1718) =< s(1621)
s(1717) =< aux(283)+aux(282)
s(1718) =< aux(283)+aux(282)
s(1719) =< s(1717)
s(1720) =< aux(283)
s(1721) =< aux(283)
s(1720) =< s(1618)+aux(283)
s(1721) =< s(1618)+aux(283)
s(1722) =< s(1720)

with precondition: [V>=0,V1>=0]

* Chain [42]: 1
with precondition: [V1=0,V>=0]


Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [43] with precondition: [V>=0,V1>=0]
- Upper bound: 414*V+689*V1+476+ (V+V1)* (420*V1)+ (V+V1)* (nat(V+V1-1)*42)+ (1961*V+1961*V1)+ (1428*V+1428*V1)* (V+V1)+ (54*V+54)+ (99*V1+99)+ (114*V+114*V1+114)
- Complexity: n^2
* Chain [42] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant

### Maximum cost of start(V,V1): 414*V+689*V1+475+ (V+V1)* (420*V1)+ (V+V1)* (nat(V+V1-1)*42)+ (1961*V+1961*V1)+ (1428*V+1428*V1)* (V+V1)+ (54*V+54)+ (99*V1+99)+ (114*V+114*V1+114)+1
Asymptotic class: n^2
* Total analysis performed in 6857 ms.

(12) BOUNDS(1, n^2)